Groups
Sign in
Groups
CProver Support
Conversations
About
Send feedback
Help
CProver Support
Contact owners and managers
1–30 of 372
Mark all as read
Report group
0 selected
Niccolo Hamilton
Jun 20
How to do correct verification correctly using hw-cbmc
I find that current hw-cbmc will get false result when verifying all programs including the
unread,
How to do correct verification correctly using hw-cbmc
I find that current hw-cbmc will get false result when verifying all programs including the
Jun 20
Arnab Ray
,
Daniel Kroening
5
Mar 17
About CNF DIMACS formula
Thanks a lot Daniel. I've one more question. Is there a way in cbmc to provide custom assertions
unread,
About CNF DIMACS formula
Thanks a lot Daniel. I've one more question. Is there a way in cbmc to provide custom assertions
Mar 17
Arjya Das
,
Nyx Brain, Martin
2
Mar 12
STL support
On Fri, 2024-03-08 at 22:17 -0800, 'Arjya Das' via CProver Support wrote: > > Hi, >
unread,
STL support
On Fri, 2024-03-08 at 22:17 -0800, 'Arjya Das' via CProver Support wrote: > > Hi, >
Mar 12
Alexander Gnusin
,
Daniel Kroening
2
9/13/23
Initialization values in EBMC
May I first ask whether you are absolutely sure that your synthesis tool chain guarantees that all
unread,
Initialization values in EBMC
May I first ask whether you are absolutely sure that your synthesis tool chain guarantees that all
9/13/23
Ruochen Dai
2/27/23
EBMC generate wrong counter-example
Dear EBMC team, I run the EBMC to detect hardware Trojans named RS232-T600 from TrustHub, however,
unread,
EBMC generate wrong counter-example
Dear EBMC team, I run the EBMC to detect hardware Trojans named RS232-T600 from TrustHub, however,
2/27/23
Sepideh Asadi
3/17/22
CBMC front-end support on C++ template instantiation
Dear CBMC team, I'm interested in verifying C++ with STL Containers via Predicate Abstraction, in
unread,
CBMC front-end support on C++ template instantiation
Dear CBMC team, I'm interested in verifying C++ with STL Containers via Predicate Abstraction, in
3/17/22
reico ming
,
Thomas Spriggs
2
10/22/21
cbmc generated 0 vcc(s), always successful
Hi Assuming you were expecting cbmc to detect the out of bounds array access, you need to pass the --
unread,
cbmc generated 0 vcc(s), always successful
Hi Assuming you were expecting cbmc to detect the out of bounds array access, you need to pass the --
10/22/21
Chester Wong
,
Martin Nyx Brain
4
8/3/21
__CPROVER_floatbv binary assignment
On Tue, 2021-08-03 at 02:12 -0700, Chester Wong wrote: > Thank you very much for your reply! >
unread,
__CPROVER_floatbv binary assignment
On Tue, 2021-08-03 at 02:12 -0700, Chester Wong wrote: > Thank you very much for your reply! >
8/3/21
Markus Toran
, …
Martin Nyx Brain
5
7/30/21
Using MathSAT SMT2 not possible
On Fri, 2021-07-30 at 07:22 -0700, Markus Toran wrote: > Hi > > Thanks for the quick reply,
unread,
Using MathSAT SMT2 not possible
On Fri, 2021-07-30 at 07:22 -0700, Markus Toran wrote: > Hi > > Thanks for the quick reply,
7/30/21
Dinesh Kumar
,
Martin Nyx Brain
8
7/30/21
What to do when SAT solver runs out of memory
On Thu, 2021-07-29 at 05:00 -0700, Dinesh Kumar wrote: > Dear Martin, > > I am able to find
unread,
What to do when SAT solver runs out of memory
On Thu, 2021-07-29 at 05:00 -0700, Dinesh Kumar wrote: > Dear Martin, > > I am able to find
7/30/21
Chester Wong
,
Martin Nyx Brain
2
7/21/21
SMT2 and goto-cc
On Tue, 2021-07-20 at 09:23 -0700, Chester Wong wrote: > > Hi, > > > > I am a new
unread,
SMT2 and goto-cc
On Tue, 2021-07-20 at 09:23 -0700, Chester Wong wrote: > > Hi, > > > > I am a new
7/21/21
martin...@gmail.com
,
Martin Nyx Brain
2
6/23/21
Detecting deep bugs with CBMC
On Wed, 2021-06-23 at 02:00 -0700, martin...@gmail.com wrote: > Hi all, > > I am wondering
unread,
Detecting deep bugs with CBMC
On Wed, 2021-06-23 at 02:00 -0700, martin...@gmail.com wrote: > Hi all, > > I am wondering
6/23/21
Andreas Tiemeyer
,
Martin Nyx Brain
4
6/11/21
Programmatic expression for the size of a CPROVER_bitvector
On Wed, 2021-06-09 at 22:52 -0700, Andreas Tiemeyer wrote: > What we are looking for is a version
unread,
Programmatic expression for the size of a CPROVER_bitvector
On Wed, 2021-06-09 at 22:52 -0700, Andreas Tiemeyer wrote: > What we are looking for is a version
6/11/21
Ramon Bejar Torres
,
Martin Nyx Brain
3
5/26/21
weird behaviour of assume with function arguments ?
On Wed, 2021-05-26 at 08:23 -0700, Ramon Bejar Torres wrote: > Hi All, > I have found while
unread,
weird behaviour of assume with function arguments ?
On Wed, 2021-05-26 at 08:23 -0700, Ramon Bejar Torres wrote: > Hi All, > I have found while
5/26/21
Reza behzadi
,
Martin Nyx Brain
2
4/29/21
ebmc conflict assignment
On Tue, 2021-04-27 at 11:29 -0700, Reza behzadi wrote: > Hello. I am a graduate student. > The
unread,
ebmc conflict assignment
On Tue, 2021-04-27 at 11:29 -0700, Reza behzadi wrote: > Hello. I am a graduate student. > The
4/29/21
Sepideh Asadi
,
Martin Nyx Brain
7
2/14/21
verifying a program with struct without field-sensitivity in Cprover5.12
On Sun, 2021-02-14 at 17:33 +0100, Sepideh Asadi wrote: > Thanks Martin for the suggestions! we
unread,
verifying a program with struct without field-sensitivity in Cprover5.12
On Sun, 2021-02-14 at 17:33 +0100, Sepideh Asadi wrote: > Thanks Martin for the suggestions! we
2/14/21
R. Kudos
, …
Hannes Steffenhagen
3
11/16/20
Exploring Formula Size vs SAT Difficulty
I should point out we did actually have some cases recently where memory usage, not performance, was
unread,
Exploring Formula Size vs SAT Difficulty
I should point out we did actually have some cases recently where memory usage, not performance, was
11/16/20
Georgi Guninski
, …
Martin Nyx Brain
3
11/9/20
Has cbmc found security bug in a widely used software?
On Sun, 2020-11-08 at 11:03 +0200, Georgi Guninski wrote: > There is a lot money in the security
unread,
Has cbmc found security bug in a widely used software?
On Sun, 2020-11-08 at 11:03 +0200, Georgi Guninski wrote: > There is a lot money in the security
11/9/20
Georgi Guninski
,
Martin Nyx Brain
4
11/6/20
Can cbmc minimize $long f(nondet long X)$?
On Wed, 2020-11-04 at 11:30 +0200, Georgi Guninski wrote: > On Tue, Nov 3, 2020 at 6:26 PM Martin
unread,
Can cbmc minimize $long f(nondet long X)$?
On Wed, 2020-11-04 at 11:30 +0200, Georgi Guninski wrote: > On Tue, Nov 3, 2020 at 6:26 PM Martin
11/6/20
Sepideh Asadi
3/23/20
Generating GOTO Program failed with Numeric exception
Dear CProver developers, when I was trying to verify a C program using CBMC-5.12 I got an error in
unread,
Generating GOTO Program failed with Numeric exception
Dear CProver developers, when I was trying to verify a C program using CBMC-5.12 I got an error in
3/23/20
Dinesh Kumar
,
Martin Nyx Brain
2
3/16/20
real path failed: cannot allocate memory
On Mon, 2020-03-16 at 05:37 -0700, Dinesh Kumar wrote: > Hi, > > I am trying to use CBMC (
unread,
real path failed: cannot allocate memory
On Mon, 2020-03-16 at 05:37 -0700, Dinesh Kumar wrote: > Hi, > > I am trying to use CBMC (
3/16/20
Peter Schrammel
3/12/20
Re: Specifiy unwind bound for recursion loop
There's already a ticket for this: https://github.com/diffblue/cbmc/issues/1680 Yes, it would be
unread,
Re: Specifiy unwind bound for recursion loop
There's already a ticket for this: https://github.com/diffblue/cbmc/issues/1680 Yes, it would be
3/12/20
Michael
,
Martin Nyx Brain
2
12/16/19
Non-Determinism for Java objects in JBMC
On Mon, 2019-12-16 at 04:34 -0800, Michael wrote: > Hi there, > > I have a question
unread,
Non-Determinism for Java objects in JBMC
On Mon, 2019-12-16 at 04:34 -0800, Michael wrote: > Hi there, > > I have a question
12/16/19
Song YANG
,
Martin Nyx Brain
2
12/10/19
invariant check failed
On Tue, 2019-12-10 at 02:32 -0800, Song YANG wrote: > Hello, > I got errors such as invariant
unread,
invariant check failed
On Tue, 2019-12-10 at 02:32 -0800, Song YANG wrote: > Hello, > I got errors such as invariant
12/10/19
pmo
,
Michael Tautschnig
4
10/7/19
cannot unpack struct with non-byte aligned component
If you could share details about the struct (in some anonymised form) and maybe create an example as
unread,
cannot unpack struct with non-byte aligned component
If you could share details about the struct (in some anonymised form) and maybe create an example as
10/7/19
pmo
,
Martin Nyx Brain
2
9/27/19
implementation-defined aspects
On Fri, 2019-09-27 at 02:23 -0700, pmo wrote: > In the C standard (C90/C99), type int is by
unread,
implementation-defined aspects
On Fri, 2019-09-27 at 02:23 -0700, pmo wrote: > In the C standard (C90/C99), type int is by
9/27/19
rumia masburah
,
Martin Nyx Brain
2
9/17/19
Comment section of dimacs format
On Mon, 2019-09-16 at 06:57 -0700, rumia masburah wrote: > Hi , > > Consider the following C
unread,
Comment section of dimacs format
On Mon, 2019-09-16 at 06:57 -0700, rumia masburah wrote: > Hi , > > Consider the following C
9/17/19
Sunandan Adhikary
, …
Martin Nyx Brain
3
8/20/19
Getting NAN as trace even after using isnormal()
On Tue, 2019-08-20 at 11:48 +0530, Sunandan Adhikary wrote: > HI, > I am trying to generate a
unread,
Getting NAN as trace even after using isnormal()
On Tue, 2019-08-20 at 11:48 +0530, Sunandan Adhikary wrote: > HI, > I am trying to generate a
8/20/19
Martin Nyx Brain
8/19/19
Re: CBMC eclipse plugin on Eclipse Version 4.12.0
On Mon, 2019-08-19 at 03:16 -0700, fauzia ehsan wrote: > Hi, > I'm trying to install
unread,
Re: CBMC eclipse plugin on Eclipse Version 4.12.0
On Mon, 2019-08-19 at 03:16 -0700, fauzia ehsan wrote: > Hi, > I'm trying to install
8/19/19
Prasuna Saka
,
Martin Nyx Brain
3
8/19/19
CPROVER Plugin for Visual Studio
Thank you for the information. Regards, Prasuna On Fri, Aug 16, 2019 at 6:49 PM Martin Nyx Brain <
unread,
CPROVER Plugin for Visual Studio
Thank you for the information. Regards, Prasuna On Fri, Aug 16, 2019 at 6:49 PM Martin Nyx Brain <
8/19/19
